PR summary cd84f88c8e

Import changes for modified files

No significant changes to the import graph

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

Current commit cd84f88c8e
Reference commit b8219087d9

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Comments from #25481 :

Me: The reason all the changes are there is that I define smul at the same time as defining the Algebra instance. The smul isn't an instance so I avoided making it. Another approach is to define rightAlgebra_smul : SMul A (A ⊗[R] B), make it locally an instance, make some API for it (some simp lemmas e.g. smul_def), and then tidy the proofs up a bit. But I was a bit concerned about making simp lemmas which only fired for a scalar multiplication which wasn't an instance so I decided to mess with simp as little as possible. I did add one simp lemma for rightAlgebra though; this was to make a proof which was added in #22933 compile again. I could remove the simp lemma and fix the #22933 proof in a different way (probably with another change) or I could alternatively add more simp lemmas about these not-usually-instances. I wasn't sure which way to go so we now have some kind of half-way house.

Me (after the old PR was delegated to me -- but I didn't merge): @eric-wieser this has been delegated to me but I am reluctant to merge because IIRC we had a discussion about this on Zulip and you were not enthusiastic about the change: your specific comment is here #mathlib4 > Right actions on tensor products (again) @ 💬 and I don't want to be the intentional causer of trouble. I do not understand the issues well enough to understand your comment properly.

I've just reread the long thread #mathlib4 > Right actions on tensor products (again) @ 💬 again and what it seems to be is a lot of stuff which is irrelevant to this PR, and then Andrew suggesting this approach, and then Eric saying "I think pulling through comm is going to cause trouble in an eventual bimodule world, where you can't commute without also moving to MulOpposite".